Nuprl Lemma : msg-form-join
0,22
postcript
pdf
A
,
B
:MsgAForm.
A
B
MsgAForm
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
Lemmas
msg-form
wf
origin
A, B:MsgAForm. A 
B 
MsgAForm A, B:MsgAForm. A B MsgAForm x:A. B(x) T